Consider the TRS R consisting of the rewrite rules
1:
gcd(x,0)
→ x
2:
gcd(0,y)
→ y
3:
gcd(s(x),s(y))
→ if(x < y,gcd(s(x),y - x),gcd(x - y,s(y)))
There are 2 dependency pairs:
4:
GCD(s(x),s(y))
→ GCD(s(x),y - x)
5:
GCD(s(x),s(y))
→ GCD(x - y,s(y))
The approximated dependency graph contains no SCCs
and hence the TRS is trivially terminating.
Tyrolean Termination Tool (0.01 seconds)
--- May 3, 2006